f2(0, y) -> y
f2(x, 0) -> x
f2(i1(x), y) -> i1(x)
f2(f2(x, y), z) -> f2(x, f2(y, z))
f2(g2(x, y), z) -> g2(f2(x, z), f2(y, z))
f2(1, g2(x, y)) -> x
f2(2, g2(x, y)) -> y
↳ QTRS
↳ DependencyPairsProof
f2(0, y) -> y
f2(x, 0) -> x
f2(i1(x), y) -> i1(x)
f2(f2(x, y), z) -> f2(x, f2(y, z))
f2(g2(x, y), z) -> g2(f2(x, z), f2(y, z))
f2(1, g2(x, y)) -> x
f2(2, g2(x, y)) -> y
F2(g2(x, y), z) -> F2(y, z)
F2(g2(x, y), z) -> F2(x, z)
F2(f2(x, y), z) -> F2(x, f2(y, z))
F2(f2(x, y), z) -> F2(y, z)
f2(0, y) -> y
f2(x, 0) -> x
f2(i1(x), y) -> i1(x)
f2(f2(x, y), z) -> f2(x, f2(y, z))
f2(g2(x, y), z) -> g2(f2(x, z), f2(y, z))
f2(1, g2(x, y)) -> x
f2(2, g2(x, y)) -> y
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
F2(g2(x, y), z) -> F2(y, z)
F2(g2(x, y), z) -> F2(x, z)
F2(f2(x, y), z) -> F2(x, f2(y, z))
F2(f2(x, y), z) -> F2(y, z)
f2(0, y) -> y
f2(x, 0) -> x
f2(i1(x), y) -> i1(x)
f2(f2(x, y), z) -> f2(x, f2(y, z))
f2(g2(x, y), z) -> g2(f2(x, z), f2(y, z))
f2(1, g2(x, y)) -> x
f2(2, g2(x, y)) -> y
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F2(g2(x, y), z) -> F2(y, z)
F2(g2(x, y), z) -> F2(x, z)
F2(f2(x, y), z) -> F2(x, f2(y, z))
F2(f2(x, y), z) -> F2(y, z)
POL(0) = 0
POL(1) = 0
POL(2) = 0
POL(F2(x1, x2)) = x1
POL(f2(x1, x2)) = 1 + 2·x1 + 2·x2
POL(g2(x1, x2)) = 2 + 2·x1 + 2·x2
POL(i1(x1)) = 2 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
f2(0, y) -> y
f2(x, 0) -> x
f2(i1(x), y) -> i1(x)
f2(f2(x, y), z) -> f2(x, f2(y, z))
f2(g2(x, y), z) -> g2(f2(x, z), f2(y, z))
f2(1, g2(x, y)) -> x
f2(2, g2(x, y)) -> y